\section{Introduction}
In this essay we present our findings for implementing a Sokoban Solver with Binary Decision Diagrams. This essay is made up of three sections. We first cover our implementation choices. In particular the architecture of our model checker, the encoding of the Binary Decision Diagrams, our reachability algorithm and the generation of a witness.
In the second section we discuss the features we implemented, the capabilities of our model checker and the performance of the model checker. Lastly we discuss how the reader can reproduce our results.
